Intended Change

A regularly occuring problem (at least in my case) is that KeY could not close a proof on DefOps and I had to switch to Model Search which closed it.

What closed the problem at the end was the use of the cross multiplication not the systematic cuts or equation saturation performed by Model Search.

An example that could not be proven w/o switching to Model Search is

public class MatrixImplem {    
    //@ public invariant x>=0 && y>=0;
    private final int x;
    private final int y;
        
    //@ public invariant matrix_implem.length == x * y; 
    private /*@spec_public @*/ int[] matrix_implem;   
        
    /*@ public normal_behavior
      @ requires i >= 0 && i < x && j >= 0 && j < y;
      @ ensures \result == matrix_implem[x * j + i];
      @ assignable \strictly_nothing;
      @*/
    public /*@ pure @*/ int get (int i, int j) {
        return matrix_implem[x * j + i];
    }   
}

The reason why cross multiplication handling was not on DefOps is that it could drown out other theories. This PR activates cross-multiplication in a restricted form for DefOps. The cross multiplication rules are restricted to cases where the product of the left-hand sides of the involved inequations occurs on some other inequation on the left side too.

Type of pull request

• New feature (non-breaking change which adds functionality)
• There are changes to the (Java) code
• There are changes to the taclet rule base: Only changes to the rulesets not to the soundness critical rule core

Ensuring quality

• New regression test DefOpsCrossMultiplicationTest with the pure arithmetic
  core of the matrix obligation (crossMultDefOps.key): closes with DefOps
  (new) and with Model Search (as before), stays open with Basic.
• Full runAllProofs on the branch: 674/674 proofs, 0 failures.
• Examples using Model Search verified byte-identical on an arithmetic proof corpus (identical
  node counts).

Additional information and contact(s)

The strategy-side surface of this PR (per-mode bindings in IntegerStrategy)
overlaps with the value-preserving cost refactoring in #3904; whichever lands
second needs a small mechanical rebase there.

PR created with AI tooling support.

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.